\section{Approach\Comment{Technique}}

\tname{} relates memory accesses observed during state-space
exploration to infer likely races.  At conceptual level,
Figures~\ref{fig:approach}~and~\ref{fig:rabbit} illustrate \tname{}'s
approach.

%%   Consider that a program model checker produces two schedules
%%   ``sched.1'' and ``sched.2'' for the subject under test.  The
%%   approach used by \tname{} is to monitor \emph{distinct} accesses to
%%   the memory and to analyze this information on-the-fly.  It stores
%%   access-related information per object and per field.  In this
%%   scenario, \tname{} is able to identify that accesses a1 and a2
%%   observed with different schedules are conflicting (see box
%% \label{sec:approach}
%% Confirming the race can be very costly as number of schedules the
%% model checker may need to produce is typically combinatorial.  On the
%% other hand, note that such combination that \tname{} created may not
%% actually occur due to the causal dependencies that may exist (and we
%% do not track) associated with the execution of a1 or a2 (see
%% Section~\ref{sec:limitations}).\Comment{ The hypothesis of \tname{} is
%%   that lack of awareness of causal dependencies will not play}

%%\vspace{1ex}\noindent\textbf{Monitoring.} 

\vspace{0.5ex}\noindent\textbf{Overview.}  \tname{} works by
monitoring the execution of instructions during state-space
exploration.  Let us assume that the tuple
$\langle{}R,o,f,t,\mathit{ls}\rangle$ denotes a read access ($R$ for
read and $W$ for write) on field $o.f$ from thread $t$ using lockset
$ls$.  Consider, for example, that \tname{} receives notification of
such an event during exploration and that previously it observed,
possibly along a different path, a write access of the form
$\langle{}W,o,f,t',\mathit{ls'}\rangle$, where $t \neq t'$ and
$\mathit{ls}~\cap~\mathit{ls'}=\emptyset$.  \tname{} considers that this
pair of accesses reveals a potential conflict: the memory
location was the same, the read and write accesses were realized by
different threads, and the locksets used to protect the data were
disjoint.  \tname{} reports this threat to the user as a warning only
if it is distinct from previously reported warnings and if it fails a
test that indicates a particular (simple) case of causality (see
Section~\ref{sec:monitoring}).  Even though the cost of this approach
is quadratic on the number of memory accesses, we only compare
accesses to the same memory locations.


\subsection{Pseudo-code}
\label{sec:monitoring}

We implemented \tname{} with a listener of Java bytecodes.  The
listener receives notifications prior to the execution of instructions
instructions that modify the heap or the static area.  The listener
searches for potential races that can be activated subject to those
notifications.\Comment{, namely the bytecode instructions
  \CodeIn{PUTFIELD}, \CodeIn{GETFIELD}, \CodeIn{PUTSTATIC}, and
  \CodeIn{GETSTATIC}.}  Figure~\ref{fig:pseudo-code} presents the
pseudo-code of \tname{}.  It uses two supporting data-structures to
encapsulate analysis data.  The class \CodeIn{MemAccess} represents a
memory access and stores related information such as the instruction
that generated the access (\CodeIn{insn}), the id of the target object
(\CodeIn{objref}\Comment{; \fix{stores -1 on static field accesses
    --na verdade, estamos gerando um hash com o nome da classe para
    definir os objRef de static fields }}), metadata about which field
of that object was the target of the access (\CodeIn{fi}), the thread
that generated the access (\CodeIn{ti}), the locks held by that thread
at that moment (\CodeIn{ls}), and the set of live threads at that
moment (\CodeIn{live}).  The class \CodeIn{WarningInfo} represents a
potential race and stores a pair of \CodeIn{MemAccess} objects
(\CodeIn{ma1} and \CodeIn{ma2}).  The state of the listener consists
of a history of memory accesses (\CodeIn{rwset}) and a set of warnings
(\CodeIn{warnings}) that \tname{} has already reported on output.  We
use the historical data to relate current with previous memory
accesses and use the set of stored warnings to avoid reporting to the
user similar/duplicate warnings that often happens, specially for
systems with symetric threads.  We organized the memory access history
as a nested map so to efficiently retrieve the set of observed
accesses on a given field of a given object at the moment the listener
observes a new access.

\lstset{escapeinside={\%*}{*)}}
\subfiguretopcaptrue
\begin{figure}[t!]
  \centering
  \begin{small}
      \lstinputlisting[language=java,
        \Comment{numbers=left,numbersep=1pt,}basicstyle=\tiny]{chapters/approach/rabbit-pseudoCodigo.java}
    \caption{\label{fig:pseudo-code}\tname{}'s pseudo-code.}
  \end{small}
  \figtabsep{}
  \vspace{-2ex}
\end{figure}


The method \CodeIn{executeInstruction} represents \tname{}'s listener.
It is called before the execution of each instruction and returns
immediately if the instruction argument is not an instruction that
manipulates a (static or instance) field (\CodeIn{PUTFIELD},
\CodeIn{GETFIELD}, \CodeIn{PUTSTATIC}, and \CodeIn{GETSTATIC}).  This
method accesses the state of the program to obtain all relevant
information necessary to build a memory access object (e.g., object
id, thread id, etc.).  It then calls method \CodeIn{checkRace} passing
this object as argument.  This call may result in the addition of a
warning to the set of warnings (\CodeIn{warnings}).  Finally,
execution calls the method \CodeIn{updateRWSet} to add the memory
access object to the access history (\CodeIn{rwset}).  To save space,
we omit the definition of this method and methods that access the
state of the program under test (\CodeIn{get*}).

The method \CodeIn{checkRace} plays a key role in \tname{}.  It
receives a memory access as argument and checks, by comparing this
access with previous accesses, if it can lead to a potential race.  The
method iterates through all previously observed memory accesses
(\CodeIn{ma2}) that target the same object and field as the current
access.  If both are read accesses, then that pair cannot lead to a
race and execution continues to the next access.  Otherwise, if the
locksets held on each access are disjoint then execution builds a
\CodeIn{WarningInfo} object denoting a likely race.  In the sequence,
execution checks if it is worth reporting this warning to the user.
We elaborate these additional checks in the following.

\vspace{0.5ex}\noindent\textbf{Optimization 1: Live threads check.}
Conceptually, we would like \tname{} to identify whether or not the
two events from a warning are causally related.  However, it is not
only expensive to obtain such information in the context of model
checking but also challenging to do it precisely when events originate
from multiple exploration paths.  We propose a simple heuristic to
partially deal with this problem.  We only report a warning if both
threads that generated the access (i.e., \CodeIn{ma1.ti} and
\CodeIn{ma2.ti}) are alive at the moment of each other access (see
step 2).  This simple check defined with method
\CodeIn{WarningInfo.areThreadsSpawned} can capture a simple form of
causal relationship.  For example, without this check \tname{}
reported additional false warnings for the subjects\Comment{\fix{estes
    subjects ainda reportam falsos warning, só que em menor numero}}
\CodeIn{airline}, \CodeIn{raxExt}, \CodeIn{twostages}, and
\CodeIn{wronglock} (see Table~\ref{table:main}).  The scenario is
manifested when, for example, one thread $t_1$ constructs an object
$o_1$, which is not accessed by $t_1$ later, and passes that object to
the constructor of thread $t_2$, which is spawned by $t_1$.  Thread
$t_2$ later accesses some field of $o_1$.  Note that when $t_1$
accesses $o_1$, $t_2$ is not spawned and when $t_2$ is spawned $t_1$
will never access $o_1$ again.

\vspace{0.5ex}\noindent\textbf{Optimization 2: Handling Symmetric
  threads.}  Conceptually, we do not want to show repeated warnings
for the case where the race can be manifested through different
combinations of symmetric threads.  To deal with that we check if the
warning is similar to another that has been observed in the past (see
step 3).  The method \CodeIn{MemAccessNo.eqNoThread} defines this
check.  We observed that two race warnings that involve the same
program locations and objects is sometimes manifested by different
pairs of threads.  This happens for the cases where the application
contains symmetric threads~\citep{clarke99:model}.  All subjects from
group 1 (see Table~\ref{table:main}) with the exception of
\CodeIn{weblench} contain symmetric threads.

%% We used two data-structures to store analysis data.  The first stores
%% memory access information; it is the raw data for our analysis.  The
%% other data-structure stores information about the potential conflicts
%% observed up to a given moment in the search; this information is
%% obtained from the raw data.  \tname{} checks if a new memory access
%% that the model checker notifies to the listener represents potential
%% race; it compares the new observation with historical data.


%% \tname{} filters similar detected conflicts.  For example, we observed
%% that several of the conflicting accesses initially reported in our
%% experiments were symmetric with respect to the threads involved.  The
%% access pattern was the same, but the threads involved in the
%% manifestation of the race were different.  In such cases, we report
%% only one representative of the symmetry class, significantly reducing
%% the number of reported warnings.

\subsection{Object Ids}  
\label{sec:objectIDs}

\lstset{escapeinside={\%*}{*)}}
\subfiguretopcaptrue
\begin{figure}[t]
  \centering
  \begin{small}
    \includegraphics[scale=0.65]{chapters/approach/objids.pdf}
  \end{small}
  \caption{\label{fig:objids}Two problems: (a) same object with
    different ids across distinct paths, and (b) different objects
    with same ids across distinct paths.}  \figtabsep{}
\end{figure}

\tname{} is applicable to a popular class of model
checkers that manipulate the state of the program explicitly.\Comment{
  to perform key model-checking operations, namely, execution,
  state-comparison, and backtracking.}  Java PathFinder (JPF), for
example, uses one array of integers to represent one object and uses
one array of integer arrays to represent the entire heap.  When JPF
needs to explore a different path, it needs to backtrack state and
that results in updating such arrays.

The identifiers that the model checker assigns to the objects created
during the state-space exploration, including monitors and threads,
are important to \tname{}: memory accesses are only comparable if they
refer to the same memory location.  We do not want \tname{} (a) to
report spurious warnings because the model checker assigned the same
id to semantically distinct objects across different exploration
paths.  Likewise, we do not want \tname{} (b) to miss a race because
the model checker assigned different ids to the same object across
different exploration paths.  Figure~\ref{fig:objids} highlights these
problems.  A broken line denotes one execution path to assignment
\CodeIn{T x = new T(...)} and a triangle denotes all subpaths from one
of such paths.  Note that the id assigned to one object will remain
fixed on all subpaths (which the triangles denote) from one given
execution path, however, the id for the same object will not
necessarily remain fixed across differen paths.  For example, a
different number of objects could have been created along the
execution path 2 compared to execution path 1.  That would result in
the assignment of a different id to the same object stored in variable
\CodeIn{x}.  Similarly, the id assigned in path 1 at \CodeIn{T x =
  ...} could be assigned to a different object in path 2.

Figure~\ref{fig:oid} shows the pseudo-code for the algorithm that
\tname{} uses to approximately compute search-global object ids.
Conceptually, it builds object ids by observing the context of
allocation expressed on the state of the stack at the moment of object
initialization (i.e., constructor invocation).  The algorithm
traverses the program stack adding integer elements denoting program
values (both reference and primitive-type) to a \CodeIn{HashData}
data-structure.  This data-structure provides a \CodeIn{getValue()}
method to compute a hash value from the integer sequence.  The
algorithm processes the operand stack of each stack frame it
encounters during the traversal, leaving out local variables which can
create noise in the characterization of objects.  \comment{For space reasons,
we ommited the treatment of arrays and Java boxed classes (such as
\CodeIn{java.lang.Integer}) from the pseudo-code.}  Finally, at line
22, the algorithm uses the method \CodeIn{setOID} to assign the
computed hash to the abstraction of the object of interest that the
model checker tracks in memory, which the expression
\CodeIn{heap.get(oref)} denotes.  Note that the object ids considered
during the stack traversal are computed with this same algorithm and
obtained with method \CodeIn{getOID}, as indicated at line 17.

\Comment{ \tname{} operates in the context of model checkers that
  manipulate the state of the program explicitly to perform key
  model-checking operations, namely, execution, state-comparison, and
  backtracking.  Java PathFinder (JPF), for example, uses one array of
  integers to represent one object and uses one array of integer
  arrays to represent the entire heap.  When JPF needs to explore a
  different path, it needs to backtrack state and that results in
  updating such arrays.  }


%\vspace{0.5ex}\noindent{}\textbf{\jpf{} implementation.} 

\lstset{escapeinside={\%*}{*)}}
\subfiguretopcaptrue
\begin{figure}[t!]
  \centering
  \begin{small}
      \lstinputlisting[language=java,
        numbers=left,numbersep=0pt,basicstyle=\tiny]{oid.java}
    \caption{\label{fig:oid}Approximate computation of search-global object Ids.}
  \end{small}
  \figtabsep{}
  \vspace{-2ex}
\end{figure}

\subsection{\jpf{} implementation}

We implemented \tname{} using the infrastructure of \jpf{}.  We
implented the code from Figures~\ref{fig:pseudo-code}
and~\ref{fig:oid} as listeners of bytecode execution.  Important to
note that \jpf{} implements a (precise) race \emph{detector} based on
the Eraser algorithm~\citep{savage-etal-1997}, but \tname{} does
\emph{not} build on JPF's race detector.  While race detectors
consider only one execution path, \tname{} considers multiple paths
using the history of memory accesses.



%% correlates objects involved across different exploration
%% paths of the program.  Unfortunately, stateful model checkers,  particularly, sometimes are not able to keep the identifier
%% of the objects fixed during exploration~\cite{lerda:01}.  The code
%% below illustrates this.\Comment{ characteristic.}

%% \small
%% \begin{verbatim}
%%   String s = "a"; if (Verify.getBoolean()) { s = "b"; /*<= comment*/ }
%%   Object x = new Object(); System.out.println(x);
%% \end{verbatim}
%% \normalsize

%% In this fragment, the JPF-provided \CodeIn{Verify.getBoolean()}
%% library call creates a non-deterministic choice, effectively forking
%% the execution path in two.  \jpf{} is unable to identify that the
%% objects assigned to variable \CodeIn{x} across both paths are in fact
%% the same.  That happens because in one of the branches execution
%% creates (and assigns) the string \CodeIn{`'b`'} (to variable
%% \CodeIn{s}) and this changes the way \jpf{} assigns ids to objects.
%% The possibility of using different ids for the same objects could lead
%% to race misses due to the inability of \tname{} to correlate memory
%% accesses.  However, note that \jpf{} will use the same identity for
%% one object across all paths created from choices that follow the
%% creation of that object.

%% \begin{figure}
%%   \centering
%%   \small
%%   \lstset{escapeinside={\%*}{*)}}
%%   \lstinputlisting[language=java,basicstyle=\scriptsize]{AlarmClock.java}
%%   \caption{\label{fig:causality}Fragment from \texttt{alarmclock}
%%     subject.  \tname{} reports a conflict in the read-write accesses
%%     to \texttt{id} even though they are causally dependent.}
%%   \vspace{-5ex}
%% %\end{wrapfigure}
%% \end{figure}
%% \normalsize


%% \subsection{Limitations}
%% \label{sec:limitations}
%% %% \tname{}'s goal is to complement model checking with earlier feedback.
%% %% The approach is lightweight and non-intrusive with respect to the
%% %% model checker behavior. 

%% We describe below key limitations of \tname{}.

%% \vspace{1ex}\noindent\textbf{Object ids.} \Fix{...}

%% \vspace{1ex}\noindent\textbf{Causality.}  \tname{} does not detect
%% causally dependent memory accesses, which by definition cannot result
%% in races.  Figure~\ref{fig:causality} illustrates one scenario that
%% \tname{} reports a false positive for this reason.  The fragment is
%% extracted and simplified from the \CodeIn{alarmclock} subject.
%% \tname{} reports such false positive very early in the search ($<$5s).
%% In this example, the main function creates a \CodeIn{Client} object
%% and initializes the field \CodeIn{id} in the context of one (main)
%% thread, then it spawns the thread associated with the client object.
%% The method \CodeIn{run} reads the field \CodeIn{id} in the context of
%% the client thread.  The field \CodeIn{id} is not protected by any lock
%% but this is not the problem.  The figure shows, as comments, the
%% vector clocks associated with each access~\cite{lamport1978}.  Each
%% element of the vector corresponds to a counter associated with each
%% thread.  Note from the values of the vectors that the read access to
%% the field is causally dependent on the store access and could not
%% result in a race.


% LocalWords:  schedules sched Fnote bytecode PUTFIELD GETFIELD PUTSTATIC JPF
% LocalWords:  GETSTATIC lockset tuple locksets stateful PathFinder getBoolean
% LocalWords:  alarmclock Online escapeinside basicstyle AlarmClock bytecodes
% LocalWords:  MemAccess insn objref checkRace
